Library line_conjugate

Require Import PointsETC.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition line_conjugate P U :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
    cTriple (p*(v^2 + w^2) - u*(q×v + r×w)) (q*(w^2 + u^2) - v*(r×w + p×u)) (r*(u^2 + v^2) - w*(p×u + q×v))
end.

End Triangle.